a, p:. prime(p)  (CoPrime(p,a)  p | a) 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, CoPrime(a,b), A, b | a, prime(a), x:A. B(x), t  T, False, a ~ b, P  Q
Lemmas	divides transitivity, prime elim, coprime intro, assoced weakening, divides weakening, coprime elim, prime wf, divides wf, not wf, coprime wf